% !Mode:: "TeX:UTF-8"
\chapter{Практическое применение, сравнение с аналогами}

В этой главе показывается, что предлагаемых в диссертации средств
описания модели состояния MMU и инструкций достаточно для генерации
тестов таких трех часто используемых архитектур как MIPS~\cite{mips64II},
PowerPC~\cite{PowerPC} и IA-32~\cite{IA32}. При
рассмотрении архитектур важными будут следующие вопросы:
\begin{enumerate}
    \item описываются ли инструкции в виде ограничений на битовые
    строки в документации?
    \item описывается ли модель состояния MMU в виде лишь таблиц? нет ли там
чего-нибудь, не сводящегося к таблице?
    \item хватает ли предлагаемых средств для описания трансляции адреса ?
\end{enumerate}

В разделе~\ref{sec:templates_estimation} описаны эксперименты по оценке длины шаблонов, для
которых удается эффективно строить тесты предлагаемыми в диссертации
методами. Заканчивается глава
сравнением особенностей предлагаемого метода генерации тестов по
тестовым шаблонам с методом, предлагаемым инструментом
Genesys-Pro~\cite{GenesysPro}.

%% отвечаем на следующие вопросы:
% 1. описываются ли инструкции в виде ограничений на битовые строки в документации
% 2. описывается ли модель состояния MMU в виде лишь таблиц? нет ли там
% чего-нибудь, не сводящегося к таблице?
% -> структура TLB
% 3. хватает ли средств для описания трансляции адреса ?
% -> поток данных, описывающих трансляцию
% режимы работы (real mode, protected mode)

% таблица - то, что представляется множеством строк,
% строка представляется набором полей ключа и полей данных

%% схема описания компонента MMU:
% 1. поля строк
% 2. количество строк
% 3. битовая длина номера региона (тип таблицы - полностью-ассоциативная, ....)
% 4. стратегия вытеснения
% 5. предикат keyMatch
% 6. особенности компонента (чего-то более одного, чего-то быть не может, ...) -
% например, одна строка хранит несколько подряд данных

% в MIPS R12000 появилась кэш-память адресов переходов (32 строки), но она не
% относится к MMU данных

\section{Генерация тестов для архитектуры MIPS}

%\begin{utv}
%Для архитектуры MIPS возможно применение применение методов, описанных в
% диссертации, для генерации тестовых программ по тестовым шаблонам; причем
% методов достаточно
% для полного описания поведения MMU микропроцессоров архитектуры MIPS.
%\end{utv}

Документация по архитектуре MIPS представлена в MIPS64™ Architecture For Programmers (в трех томах)~\cite{mips64II, mips64III}. Второй том (The MIPS64™ Instruction Set) содержит описания инструкций, которые действительно описываются в виде набора операций над битовыми строками (см.рис.~\ref{fig:mips64_page}).

\begin{figure}
\textbf{Load Doubleword    LD}\\

\textbf{Format:} LD rt, offset(base)\\

\textbf{Purpose:} To load a doubleword from memory\\

\textbf{Description:} rt <- memory[base+offset]

The contents of the 64-bit doubleword at the memory location specified by the aligned effective address are fetched and placed in GPR rt. The 16-bit signed offset is added to the contents of GPR base to form the effective address.\\

\textbf{Restrictions:}\\
The effective address must be naturally-aligned. If any of the 3 least-significant bits of the address is non-zero, an Address Error exception occurs.\\

\textbf{Operation:}
\begin{verbatim}
vAddr <- sign_extend(offset) + GPR[base]
\end{verbatim}
\texttt{if vAddr$_{2..0} \neq 0^3$ then}
\begin{verbatim}
   SignalException(AddressError)
endif
(pAddr, CCA) <- AddressTranslation (vAddr, DATA, LOAD)
memdoubleword <- LoadMemory (CCA, DOUBLEWORD, pAddr, vAddr, DATA)
GPR[rt] <- memdoubleword
\end{verbatim}

\textbf{Exceptions:}\\
TLB Refill, TLB Invalid, Bus Error, Address Error, Reserved Instruction, Watch

\caption{Пример страницы документации по системе команд архитектуры MIPS64}\label{fig:mips64_page}
\end{figure}

Третий том (The MIPS64™ Privileged Resource Architecture) содержит описание подсистемы управления памяти в
микропроцессорах MIPS. Для работы с данными она содержит следующие блоки (количественные
характеристики приведены для микропроцессора MIPS R10000~\cite{R10000}):
\begin{itemize}
  \item \emph{кэш-память данных первого уровня (D-Cache-1)}:
        \begin{itemize}
            \item размер: 32 кБ;
            \item поля строк: тэг физического адреса (ключ), данные (данные);
            \item битовая длина номера региона: 6 (наборно-ассоциативная
кэш-память);
            \item количество строк в регионе: 2;
            \item стратегия вытеснения \LRU;
        \end{itemize}
  \item \emph{кэш-память второго уровня (Cache-2)}:
        \begin{itemize}
            \item размер: от 512 кБ до 16 МБ;
            \item поля строк: тэг физического адреса для кэш-памяти второго
уровня (ключ), данные (данные) (16 или 32 слова);
            \item количество строк в регионе: 2;
            \item стратегия вытеснения \LRU;
        \end{itemize}
         Cache-2 является внешней;
  \item \emph{TLB (Joint-TLB)}:
        \begin{itemize}
            \item поля строк: r, vpn/2, g, asid (ключи), pfn0, cca0, v0, c0, d0,
pfn1, cca1, v1, c1, d1 (данные);
            \item битовая длина номера региона: 0 (полностью-ассоциативный TLB);
            \item количество строк в регионе: 64;
            \item вытеснение программное (т.е. стратегия вытеснения none);
            \item размер виртуального адреса: 44 бита;
            \item размер физического адреса: 40 бит;
        \end{itemize}
        одна строка TLB хранит информацию про две соседние страницы виртуальной
        памяти;
  \item \emph{буфер TLB (D-TLB)}:
        \begin{itemize}
            \item поля строк те же, что и для Joint-TLB;
            \item битовая длина номера региона: 0 (полностью-ассоциативный);
            \item количество строк в регионе: 8;
            \item стратегия вытеснения \LRU;
        \end{itemize}
\end{itemize}

Другие блоки для обращения в память не используются.

Осталось показать, что трансляция адреса также может быть представлена в виде
отношений на битовых строках и обращениях в таблицы. Обычное выполнение
обращения к памяти в MIPS следующее:
\begin{enumerate}
    \item на основе аргументов инструкции формируется \emph{виртуальный адрес}
(VA);
    \item заменой номера страницы виртуальной памяти на номер фрейма физической
памяти формируется \emph{физический адрес} (PA);
    \item по физическому адресу, если нужно, осуществляется обращение в
кэш-память иди, если данных по физическому адресу нет в кэш-памяти, обращение в
оперативную память.
\end{enumerate}

\begin{figure}[h] \center
  \includegraphics[width=0.8\textwidth]{4.analysis/mips_addrtrans}\\
  \caption{Трансляция адреса в MIPS}\label{fig:mips_address_translation}
\end{figure}


В зависимости от значения виртуального адреса и состояния управляющих регистров
возможны следующие варианты трансляции адреса:
\begin{itemize}
  \item для виртуального адреса трансляция проходит через TLB
(см.рис.~\ref{fig:mips_address_translation});
  \item для виртуального адреса трансляция проходит без таблиц (физический адрес
--- битовая строка --- является результатом битовых операций над виртуальным
адресом --- битовой строкой).
\end{itemize}

Пример модели инструкции LD с рисунка~\ref{fig:mips64_page} приведен в приложении~\ref{sec:xml}.

\section{Генерация тестов для архитектуры PowerPC}

Архитектура PowerPC разработана компанией IBM. Документация по архитектуре
PowerPC представлена в PowerPC Architecture Book (в трех томах)~\cite{PowerPC}. Первый том (PowerPC User Instruction Set Architecture) содержит описания инструкций, которые действительно описываются в виде набора операций над битовыми строками (см.рис.~\ref{fig:ppc_page}.

\begin{figure}
\textbf{Store Halfword Indexed X-form}

sthx RS,RA,RB

\begin{verbatim}
if RA = 0 then b <- 0
else           b <- (RA)
EA <- b + (RB)
MEM(EA, 2) <- (RS)48:63
\end{verbatim}

Let the effective address \texttt{(EA)} be the sum \texttt{(RA|0)+(RB)}. \texttt{(RS)48:63} are stored into the halfword in storage addressed by \texttt{EA}.\\

\textbf{Special Registers Altered:}\\
None
\caption{Пример страницы документации системы команд PowerPC}\label{fig:ppc_page}
\end{figure}

Третий том (PowerPC Operating Environment Architecture) содержит описание подсистемы управления памяти в микропроцессорах PowerPC. Для работы с данными она содержит следующие блоки (количественные характеристики приведены для микропроцессора PowerPC 970FX
~\cite{PowerPC970FXUserManual}):
\begin{itemize}
  \item \emph{кэш-память данных первого уровня (D-Cache-1)}:
        \begin{itemize}
            \item размер: 32 кБ;
            \item поля строк: тэг физического адреса (ключ), данные (данные);
            \item битовая длина номера региона: 7 (наборно-ассоциативная
кэш-память);
            \item количество строк в регионе: 2;
            \item стратегия вытеснения \LRU;
        \end{itemize}
  \item \emph{кэш-память второго уровня (Cache-2)}:
        \begin{itemize}
            \item размер: 512 кБ;
            \item поля строк: тэг физического адреса (ключ), данные (данные);
            \item битовая длина номера региона: 11 (наборно-ассоциативная
кэш~--~память);
            \item количество строк в регионе: 8;
            \item стратегия вытеснения \LRU;
        \end{itemize}
  \item \emph{D-TLB} (кэш таблицы страниц):
        \begin{itemize}
            \item поля строк: номер страницы виртуальной памяти (ключ), номер
фрейма физической памяти (данные);
            \item битовая длина номера региона: 8 (наборно-ассоциативный);
            \item количество строк в регионе: 4;
            \item стратегия вытеснения \LRU;
        \end{itemize}
  \item \emph{сегментные регистры (SLB, Segment Lookaside Buffer)}:
        \begin{itemize}
            \item поля строк: effective segment id (ключ), virtual segment id
(данные), биты K$_s$/K$_p$, V, N, L, C (данные);
            \item битовая длина номера региона: 0 (полностью ассоциативный);
            \item количество строк в регионе: 64;
            \item вытеснение программное;
        \end{itemize}
        используются для получения виртуального адреса по эффективному;
%  \item \emph{буфер непосредственной трансляции адресов (D-ERAT)}:
% НЕТ ЭТОГО БУФЕРА В АРХИТЕКТУРЕ!!! его добавили в самом микропроцессоре
% PPC970FX
%        \begin{itemize}
%            \item поля строк: номер <<эффективной страницы>> (ключ), номер
% фрейма физической памяти (данные), биты (данные);
%            \item битовая длина номера региона: 6 (наборно-ассоциативная
% таблица);
%            \item количество строк в регионе: 2;
%            \item стратегия вытеснения \FIFO;
%        \end{itemize}
\end{itemize}

Кроме того, в оперативной памяти организуется \emph{таблица страниц виртуальной
памяти (PageTable)}. Хотя формально она не является блоком микропроцессора, но
используется при трансляции адреса, то она тоже может быть оформлена в виде
такой таблицы:
    \begin{itemize}
        \item поля строк: номер страницы виртуальной памяти (ключ), номер фрейма
физической памяти (данные);
        \item битовая длина номера региона: 65;
        \item количество строк в регионе: 1;
        \item вытеснение программное;
        \item размер эффективного адреса: 64 бита;
        \item размер виртуального адреса: 65 бит;
        \item размер физического адреса: 42 бита;
    \end{itemize}

На самом деле таблица страниц виртуальной памяти организована в виде сложной
хэш-таблицы, но для тестирования этот момент не важен --- главное, что это
соответствие номеров страниц виртуальной памяти номерам фреймов физической
памяти, причем необязательно представлены все страницы виртуальной памяти.

Другие блоки для обращения в память не используются.

Осталось показать, что трансляция адреса также может быть представлена в виде
отношений на битовых строках и обращениях в таблицы. Обычное выполнение
обращения к памяти в PowerPC следующее:
\begin{enumerate}
    \item аргументы инструкции обращения к памяти формируется \emph{эффективный
адрес} (EA);
    \item заменой номера сегмента из эффективного адреса получается
\emph{виртуальный адрес} (VA);
    \item заменой номера виртуальной страницы в виртуальном адресе на номер
фрейма физической памяти получается \emph{физический адрес} (PA);
    \item по физическому адресу, если нужно, осуществляется обращение в
кэш-память иди, если данных по физическому адресу нет в кэш-памяти, обращение в
оперативную память.
\end{enumerate}

В зависимости от состояния управляющих регистров возможны следующие варианты
трансляции адреса:
\begin{itemize}
  \item real addressing mode (трансляция выключена); физический адрес
вычисляется по эффективному без обращения к каким-либо таблицам;
  \item режим с трансляцией адреса (см. рис.~\ref{fig:ppc_address_translation}).
\end{itemize}

\begin{figure}[h] \center
  \includegraphics[width=\textwidth]{4.analysis/ppc_addrtrans}\\
  \caption{Трансляция адреса в PowerPC}\label{fig:ppc_address_translation}
\end{figure}


\section{Генерация тестов для архитектуры IA-32}

IA-32 --- это архитектура, разрабатываемая компанией Intel. Документация по
архитектуре IA-32 представлена книгой IA-32 Intel® Architecture
Software Developer’s Manual (в пяти томах)~\cite{IA32}. Второй и третий тома \\(Instruction Set Reference) содержат определения инструкций, которые действительно описываются в виде набора операций над битовыми строками (см.рис.~\ref{fig:ia32_page}).

\begin{figure}
\textbf{TEST—Logical Compare}\\

\textbf{Description}\\
Computes the bit-wise logical AND of first operand (source 1 operand) and the second operand
(source 2 operand) and sets the SF, ZF, and PF status flags according to the result. The result is
then discarded.\\

\textbf{Operation}
\begin{verbatim}
TEMP <- SRC1 AND SRC2;
SF <- MSB(TEMP);
IF TEMP = 0
  THEN ZF <- 1;
  ELSE ZF <- 0;
FI:

PF <- BitwiseXNOR(TEMP[0:7]);
CF <- 0;
OF <- 0;
(* AF is undefined *)
\end{verbatim}

\textbf{Flags Affected}\\
The OF and CF flags are set to 0. The SF, ZF, and PF flags are set according to the result (see
the "Operation" section above). The state of the AF flag is undefined.

\caption{Пример страницы документации системы команд архитектуры IA-32}\label{fig:ia32_page}
\end{figure}

Четвертый и пятый тома (System Programming Guide) содержат описание подсистемы управления памяти в
микропроцессорах IA-32. Для работы с данными она содержит следующие блоки
(количественные характеристики приведены для микропроцессора Intel Pentium
Pro~\cite{PentiumPro}) :
\begin{itemize}
  \item \emph{кэш-память данных первого уровня (D-Cache-1)}:
        \begin{itemize}
            \item размер: 8 кБ;
            \item поля строк: тег адреса (ключ), данные (данные);
            \item битовая длина номера региона: 7 (наборно-ассоциативный);
            \item количество строк в регионе: 2;
            \item стратегия вытеснения \LRU;
        \end{itemize}

  \item \emph{кэш-память второго уровня (Cache-2)}:
        \begin{itemize}
            \item размер: в разных версиях 256 кБ, 521 кБ или 1 МБ;
            \item поля строк: тег адреса (ключ), данные (данные);
            \item битовая длина номера региона: от 11 до 13 в разных версиях
(наборно-ассоциативный);
            \item количество строк в регионе: 4;
            \item стратегия вытеснения \LRU;
        \end{itemize}

  \item \emph{TLB (D-TLB)}:
        \begin{itemize}
            \item поля строк: page number (ключ), page base address (данные),
флаги (данные);
            \item битовая длина номера региона: 4 (наборно-ассоциативный);
            \item количество строк в регионе: 4;
            \item стратегия вытеснения \LRU;
        \end{itemize}

  \item \emph{таблица страниц виртуальной памяти (PageTable)}:
    \begin{itemize}
        \item поля строк: page number (ключ), page base address (данные), флаги
(данные);
        \item битовая длина номера региона: 65;
        \item количество строк в регионе: 1;
        \item вытеснение программное;
        \item размер логического адреса: 48 бит;
        \item размер линейного адреса: 32 бит;
        \item размер физического адреса: 32 бита;
    \end{itemize}


  \item \emph{таблица дескрипторов сегментов (SDT)}:
        \begin{itemize}
            \item поля строк: segment selector (ключ), база (данные), флаги
(данные);
            \item битовая длина номера региона: 13;
            \item количество строк в регионе: 1;
            \item вытеснение программное;
        \end{itemize}
\end{itemize}

Другие блоки для обращения в память не используются.

\begin{figure}[h] \center
  \includegraphics[width=0.8\textwidth]{4.analysis/ia32_addrtrans}\\
  \caption{Трансляция адреса в IA-32}\label{fig:ia32_address_translation}
\end{figure}

Осталось показать, что трансляция адреса также может быть представлена в виде
отношений на битовых строках и обращениях в таблицы. Обычное выполнение
обращения к памяти в IA-32 следующее:
\begin{enumerate}
    \item аргументы инструкции обращения к памяти формируется \emph{логический
адрес} (SS:EA);
    \item заменой номера сегмента из логического адреса получается
\emph{линейный адрес} (LA);
    \item либо линейный адрес трактуется как физический, либо заменой номера
виртуальной страницы в линейном адресе на номер фрейма физической памяти
получается физический адрес (PA);
    \item по физическому адресу, если нужно, осуществляется обращение в
кэш-память иди, если данных по физическому адресу нет в кэш-памяти, обращение в
оперативную память.
\end{enumerate}

В зависимости от состояния управляющих регистров возможны следующие варианты трансляции адреса:
\begin{itemize}
  \item real-address mode (трансляция выключена) --- физический адрес равен линейному, линейный адрес вычисляется по логическому без обращения к каким-либо таблицам;
  \item protected mode --- режим с трансляцией адреса через таблицу страниц (см. рис.~\ref{fig:ia32_address_translation}).
\end{itemize}



\section{Реализация}

Реализация генератора программ состоит из компонентов, представляющих следующие <<деятельности>> (см. рис.~\ref{fig:activities}):
\begin{figure}[h] \center
  \includegraphics[width=0.7\textwidth]{3.impl/activities1}\\
  \caption{Диаграмма деятельностей по генерации тестовых программ}\label{fig:activities}
\end{figure}
\begin{enumerate}
  \item генерация тестовых шаблонов;
  \item синтаксический анализ исходных текстовых данных; создается внутреннее представление шаблона, моделей блоков, моделей вариантов инструкций для других компонентов;
  \item генерация (текстов) ограничений с использованием описанных в разделах~\ref{sec:constraints_generation_section} и \ref{sec:usefulness_functions} методов (smt~\cite{SMT}); кроме того строится структура, хранящая семантическую информацию о созданных переменных в ограничениях;
  \item обертка решателя ограничений; вызывается внешний решатель ограничений, берется результат его работы, извлекаются из него значения переменных и эти значения прописываются в созданной ранее структуре;
  \item конструирование текстов программ на основе внутреннего представления шаблона и значениях переменных.
\end{enumerate}

Реализация для модельного микропроцессора архитектуры MIPS64~\cite{mips64II} включала следующие компоненты:
\begin{itemize}
  \item генератор тестовых шаблонов внешний --- MicroTESK~\cite{MicroTESK};
  \item решатель ограничений внешний --- Z3~\cite{Z3};
  \item синтаксический анализ моделей, генерация текстов ограничений, обертка решателя ограничений --- компонент <<Генератор ограничений>> на Ruby (порядка 2000 строк);
  \item конструирование тестовых программ --- компонент на Java (порядка 500 строк).
\end{itemize}

Типичный размер модели варианта инструкции --- 100 строк (в представлении на xml). Типичный размер модели блока --- 20 строк (в представлении на xml).

Генератор ограничений практически целиком переносим при смене архитектуры.

\section{Оценка допустимой сложности тестовых\\шаблонов}\label{sec:templates_estimation}

%эксперименты с длинами и временем генерации/процентом успешной
%генерации. Показать, что допустимая длина действительно увеличивается!

Был реализован прототип генератора ограничений для модельного микропроцессора архитектуры
MIPS64~\cite{mips64II}. В качестве решателя ограничений в нем использовался Z3~\cite{Z3}. Был проведен ряд экспериментов. Целью этих экспериментов было исследование допустимой сложности тестовых шаблонов при использовании предлагаемых в диссертации методов (под сложностью понимается
качество шаблона, пропорциональное количеству зависимых данных в нем).

В экспериментах тестовые шаблоны состояли из инструкций загрузки и сохранения
данных в памяти. В каждой инструкции должна была выполняться трансляция адреса
через TLB (с использованием D-TLB) и затем обращение в основную память через
кэш-память первого уровня. Рассматривались все длины тестовых шаблонов от 2 до
16. Для каждой длины рассматривались следующие ассоциативности кэш-памяти --- 2,
4, 8 и 16. При фиксированной длине шаблона и ассоциативности кэш-памяти
случайным образом генерировался тестовый шаблон (более конкретно, зависимости
аргументов инструкций).

Рисунки~\ref{fig:success_experiment} и~\ref{fig:time_experiment} представляют
некоторые средние значения (среднее бралось по всем тестовым шаблоном
фиксированной длины). На рисунке~\ref{fig:success_experiment} отражена доля
шаблонов, для которых был построен тест за время, меньшее чем 60 секунд (если
время превышало 60 секунд, построение теста обрывалось). На
рисунке~\ref{fig:time_experiment} отражено среднее время генерации теста (по
сути, среднее время разрешения ограничений). Более точно, среднее время
продуктивного принятия решения о тестовом шаблоне, т.е. время определения того,
что шаблон является несовместным (для него не может быть теста вовсе) или
совместным с построением теста.

Эксперименты проходили на компьютере AMD Athlon64 3200+ 2ГГц с 1ГБ оперативной
памяти.

\begin{figure}[p] \center
\parbox[t]{\textwidth}{
  \includegraphics[width=\textwidth]{4.analysis/success_exprmnt}%
\caption{Доля тестовых шаблонов, для которых удалось построить тест за 60с или
определить их несовместность}\label{fig:success_experiment}
}

\vspace{1.5cm}

\parbox[t]{\textwidth}{
  \includegraphics[width=\textwidth]{4.analysis/time_exprmnt}
  \caption{Среднее время продуктивного принятия решения о тестовом
шаблоне}\label{fig:time_experiment}
}
\end{figure}

В первой серии экспериментов (их результаты отражены на рисунках линиями с
квадратиками) генерация ограничений делалась для всего тестового шаблона.
Оказалось, что до некоторой длины шаблона (значит, и теста) (8-9) метод работает
успешно практически для всех тестовых шаблонов (97\%-100\%). При дальнейшем
увеличении длины шаблона начинает уменьшаться доля шаблонов, для которых удается
построить тест (по 5-10\% при увеличении длины теста). Тем самым при длине теста
порядка 14-15 уже для половины шаблонов решатель ограничений не успевает за 60
секунд принять решение и построить тест. В результате анализа использованных в
экспериментах тестовых шаблонов был сделан вывод, что для большинства из них
(60-70\%) тестов не может быть вовсе, так как в этих шаблонах имеются обращения
по одинаковым адресам с кэш-промахами после кэш-попаданий и кэш-промахами после
кэш-промахов (поскольку в результате кэш-промаха данные помещались в кэш-память
и при повторном обращении к ним должно происходить только кэш-попадание, а не
кэш-промах).

Поскольку эта ситуация стала по сути следствием случайного выбора тестовых
шаблонов, то в следующей серии экспериментов перед запуском генерации
ограничений была вставлена процедура, отсеивающая априори несовместные тестовые
шаблоны (т.е. такие, для которых не может существовать тестов вовсе). Кроме того
обращения в кэш-память были поделены на группы на основе одинаковых имен
аргументов и для этих групп генерировались ограничения (грубо говоря, к шаблону
добавлялось требование обращения по разным именам аргументов в разные регионы,
если это не противоречило шаблону). Результаты этой второй серии экспериментов
отражены на рисунках~\ref{fig:success_experiment} и \ref{fig:time_experiment}
линией с кружками. Из них следует, что примененные изменения позволили
дополнительно увеличить на несколько единиц допустимый размер тестового шаблона.

Для каждой пары (длина шаблона, ассоциативность) было сгенерировано 1000
тестовых шаблонов. Насколько можно доверять полученным в экспериментах
результатам на таком количестве тестовых шаблонов? Для ответа на этот вопрос воспользуемся аппаратом теории
вероятностей. Пусть $N$ --- количество испытаний. Одно испытание заключается в
следующем: сначала случайным образом строится тестовый шаблон, затем генерируются
для него ограничения и, наконец, они разрешаются. Испытание заканчивается успешно, если за отведенное время (60с) решатель ограничений построил тест, и неуспешно, если не успел построить.
Обозначим  $\xi_i$, $i = 1, 2, \dots, N$, случайные величины, соответствующие
успешности испытаний. Их областью значений будет множество $\{0, 1\}$. Эти
случайные величины независимы и одинаково распределены (обозначим $p =
\mathsf{P}\{\xi_i = 1\}$). Поэтому применим \emph{закон больших чисел}, согласно
которому $\frac{\sum_{i=1}^N \xi_i}{N} ~ p$ при <<больших>> $N$. Более точно, для любых
положительных $\varepsilon$ и $\delta$ найдется число $N^*$, что для всех $N > N^*$ будет
выполнено $\mathsf{P}\{|\frac{\sum_{i=1}^N \xi_i}{N} - p | \geq \varepsilon\} \leq \delta$. $\varepsilon$ --- это допустимое отклонение в оценке результата экспериментов (т.е. оценке $p$). $\delta$ показывает, насколько можно доверять полученному результату экспериментов. Поскольку $\sum \xi_i$ распределена по биномиальному закону ($\mathsf{P}\{\sum_{i=1}^N \xi_i = m\} = \binom{N}{m} p^m (1{-}p)^{N{-}m}$), то для вероятности отклонения более, чем на $\varepsilon$, справедлива следующая формула: $$\sum_{m = 0}^{(p-\varepsilon)N} \binom{N}{m} p^m (1{-}p)^{N{-}m} + \sum_{m = (p+\varepsilon)N}^N \binom{N}{m} p^m (1{-}p)^{N{-}m} \leq \delta$$ Эта формула позволяет оценить $\delta$ при разных $p$, зная $\varepsilon$ и $N$.

Итак, для каждого $n \in \{2,3\}$ ($n$ --- длина тестового шаблона) было сгенерировано по $B = 1000$ тестовых шаблонов. При этом получилось $p \in [0.9, 1.0]$. Если взять допустимое отклонение от истинного значения $\varepsilon = 0.02$ (2\%) (что вполне допустимо, т.к. отклонение в 2\% не сильно изменит результат эксперимента), то вероятность ошибиться в этом случае была бы не более $\delta = 0.03$, т.е. 3\%, что тоже вполне допустимо. Для $n \in \{4, 5, 6, 7\}$ было сгенерировано по $N = 2000$ тестовых шаблонов (для $w \in \{2,4\}$). Если взять $\varepsilon = 0.02$ (2\%), то для $p \in [0.9, 1.0] \delta = 0.003$, т.е. $0.3\%$, т.е. ошибка в этом случае еще меньше. И, наконец, для $n \in \{8, 9, ..., 14\}$ было сгенерировано по $N = 3000$ тестовых шаблонов, что при $\varepsilon = 0.02$ и $p \in [0.5, 1.0]$ дает $\delta = 0.02$, т.е. всего 2\%. Таким образом, вероятность ошибки в проведенных экспериментах невелика.

Проведенные эксперименты позволяют произвести сравнение с инструментом
MicroTESK~\cite{MicroTESK}. Этот инструмент был успешно применен для построения
тестов по всевозможным тестовым шаблонам из 2-3 инструкций~\cite{vorobyev}. При
увеличении длины тестового шаблона (и, соответственно, сложности) удается
строить тесты для всё меньшего количества шаблонов. Что и отражено на
рисунках~\ref{fig:success_experiment} и \ref{fig:time_experiment} линиями с
ромбами. Напротив, как показывают эксперименты, предложенные методы позволяют
строить тесты по шаблонам из 8-11 инструкций обращения к памяти. Допустимая
длина шаблонов может быть еще больше, если кроме инструкций обращения к памяти в
шаблоне используются и другие инструкции (например, арифметические).

\section{Сравнение с Genesys-Pro}

В прошлом разделе было произведено сравнение с инструментом\\
MicroTESK~\cite{MicroTESK}. В этом разделе будет произведено сравнение с другим
инструментом нацеленной генерации тестов --- Genesys-Pro~\cite{GenesysPro}. Сравнить
по эффективности и провести эксперименты с Genesys-Pro не удается, поскольку
этот инструмент не распространяется за пределы IBM. Однако имеется ряд
публикаций~\cite{GenesysPro2004Innovations, GenesysSolver}, на основе которых удалось сделать некоторое сравнение.

Технологически генерация тестов с использованием Genesys-Pro выглядит следующим
образом:
\begin{enumerate}
    \item подготовить Architectural simulator --- эталонный симулятор
микропроцессора;
    \item подготовить Architectural model --- описание системы команд
тестируемого микропроцессора с указанием для каждой инструкции набора атрибутов
и ограничений значений атрибутов (по сути, описание в виде ограничений
предусловий инструкций и вычисляемым им функций); пример описания инструкции
LoadWord изображен на рисунке~\ref{fig:GenesysProArchitecturalModel}; для
описания трансляции адреса предлагается метод DeepTrans~\cite{DeepTrans} ---
пример изображен на рисунке~\ref{fig:DeepTransExample};
    \item подготовить Test template --- тестовый шаблон; в нем задаются
инструкции теста и интересные для тестирования ситуации исполнения инструкций;
    \item подготовить Testing knowledge --- комплект ограничений на аргументы
инструкций, описывающих ситуации исполнения инструкций из test template;
    \item подготовить или использовать имеющийся решатель ограничений;
    \item запустить Genesys-Pro с подготовленными моделями.
\end{enumerate}
%% я понимаю, что такую последовательность шагов нельзя называть
%% технологической, ибо непоятно
%% 1) как выбирать Testing knowledge - что туда включать, а что нет; наверняка,
%% есть некое понимание того, что хочется протестировать; это понимание
%% должно быть формализовано (модель покрытия) и на его основе уже решать,
%% что включать в Testing knowledge, а что нет;
%% 2) не описано, как анализировать результаты Genesys-Pro: всё ли он сделал или
%% нет, надо ли дорабатывать то, что он генерирует? Надо ли как-то иначе
%% формулировать модели с шагов 1-3 для того, чтобы тесты были построены
%% целиком. И что значит "целиком"? Нет ведь модели покрытия!

\begin{figure}[h] \center
  \includegraphics[width=0.8\textwidth]{4.analysis/arch-model}
  \caption{Architectural model для инструкции
LoadWord}\label{fig:GenesysProArchitecturalModel}
\end{figure}

\begin{figure}[h] \center
  \includegraphics[width=0.8\textwidth]{4.analysis/deeptrans}
  \caption{Пример трансляции адреса в DeepTrans}\label{fig:DeepTransExample}
\end{figure}

\begin{figure}[h] \center
  \includegraphics[width=\textwidth]{4.analysis/g-pro}
  \caption{Genesys-Pro (слева) и предлагаемый в диссертации генератор
(справа)}\label{fig:GenesysProScheme}
\end{figure}

Genesys-Pro работает следующим образом: (см. левую часть
рис.~\ref{fig:GenesysProScheme})
\begin{enumerate}
    \item выбирает очередную инструкцию из Test template, для нее запрашивает
определение из Architectural model и для указанной для нее тестовой ситуации
запрашивает определение из Testing knowledge; кроме того запрашивает текущее
состояние микропроцессора у Architectural simulator;
    \item составляет из этого систему ограничений, передает их для разрешения на
costraint solver и получает ответ;
    \item формирует инструкцию и записывает ее в Test program, а также формирует
часть начального состояния (initial state);
    \item исполняет инструкцию на Architectural simulator, тот ее исполняет.
\end{enumerate}
% т.е. получается, симулятор должен быть каким-то особенным, чтобы уметь
% работать из неполного состояния? (с lazy-значениями 'X') поскольку не
% всё начальное состояние построено перед
% первой инструкций и достраивается в процессе построения теста

\paragraph{Сходства с Genesys-Pro} следующие:
\begin{itemize}
    \item подход, в котором тестовый шаблон и микропроцессор описываются
декларативным образом, и кроме этого есть независимый от них генератор, который
принимает на вход эти описания и строит тест; альтернативным решением могла быть
технология, в которой по модели вручную приходилось бы создавать дополнительные
исполнительные модули, учитывающие особенности модели микропроцессора и
тестового шаблона;
    \item использование ограничений (constraints) для построения тестов;
    \item сходные идеи есть и в методе описания трансляции адресов: Genesys-Pro
предлагает декларативное описание, в котором описываются разные варианты
трансляции с указанием того, как формируются виртуальные/физические адреса, и в
предлагаемом в диссертации подходе описывается формирование адресов; и там, и
там речь идет о \emph{таблицах}, для которых формулируются атрибуты (в том числе
и предикат типа keyMatch).
\end{itemize}

\paragraph{Отличия от Genesys-Pro} следующие:
\begin{itemize}
    \item разные принципы построения ограничений; Genesys-Pro строит тест по
одной инструкции и формулирует ограничения только для одной очередной
инструкции; напротив, в предлагаемом методе ограничения строятся для всего
тестового шаблона целиком;
    \item разные методы построения ограничений; Genesys-Pro знает всё состояние
микропроцессора целиком при формулировании ограничения на очередную инструкцию;
напротив, в предлагаемом методе ограничения состояние микропроцессора неизвестно
вообще; это приводит к ограничениям разной природы;
    \item Genesys-Pro предполагает для инструкции раздельное описание
вычисляемой функции и ограничений на входные данные; в предлагаемом методе эти
описания оформляются вместе;
    \item Genesys-Pro позволяет компактно описать длинные тесты, но важно то,
что эти возможности позволяют описывать целые классы последовательностей
инструкций;
    \item разный способ описания инструкций; Genesys-Pro предлагает делать это в
виде ограничений на атрибуты инструкции, а здесь --- в виде цепочки операторов;
    \item Genesys-Pro рассчитан на подготовку специальных решателей ограничений;
напротив, в предлагаемом методе используются сторонние решатели ограничений и
отдельно подготавливать их не нужно.
\end{itemize}

\paragraph{Преимущества и недостатки по сравнению с Genesys-Pro}:
\begin{itemize}
    \item с помощью Genesys-Pro удается строить очень длинные тесты, но не обязательно эти тесты будут сложными (иметь большое количество зависимых данных);
    \item существует тестовый шаблон, для которого существует тест, но Genesys-Pro его не построит за некоторое время (без, возможно, неописанных в публикациях эвристик), а предлагаемым в диссертации методом тест будет построен; в этом тестовом шаблоне последовательность инструкций должна быть фиксирована; а возможный пример ситуаций в шаблоне такой: в одной из инструкций должны быть вытеснены некоторые специальные данные, которых нет в текущем состоянии из-за неверного выбора данных для предыдущих инструкций;
    \item тем не менее, возможное отсутствие фиксированной цепочки дает Genesys-Pro бонус, поскольку при наличии выбор инструкции может быть успешно сделан с учетом текущего состояния микропроцессора;
    \item Genesys-Pro приходится работать с большими массивами данных (это память, всевозможные кэши и таблицы страниц), эти массивы данных участвуют в ограничениях; поэтому в решателе ограничений приходится разрабатывать методы эффективной работы с ними~\cite{GenesysSolver}; задача построение такого решателя обладает высокой сложностью (как и задача построения эффективного решателя ограничений вообще); кроме того, большая часть такого решателя может оказаться невостребованной при работе с другой моделью микропроцессора, с другим классом тестовых шаблонов --- его придется писать заново; а в предлагаемом методе разрабатывать собственные решатели не нужно.
\end{itemize}

%Genesys-Pro чётко разделяет свойства аргументов
%инструкции и свойства результата инструкции, соотношение между ними
%задается не с помощью ограничений (т.е. не декларативным способом),
%а в виде алгоритма (т.е. императивным способом).
%
%Другой особенностью Genesys-Pro является то, что поддерживаемые им
%тестовые шаблоны зачастую не фиксируют последовательность инструкций
%(это позволяет строить более простые ограничения, потому как
%генерируемая последовательность инструкций может по ходу генерации
%подстраиваться под уже сгенерированные инструкции со
%сгенерированными значениями аргументов, под состояние
%микропроцессора, в которое привели сгенерированные инструкции).
%
%Выразительный язык Genesys-Pro для описания ограничений однако
%содержит такие нетривиальные конструкции, как явное использование
%элементов массивов данных, что требует для разрешения продвинутый
%решатель CSP, в том числе и заточенный под особенности генерации
%тестовых данных для тестовых шаблонов (как минимум такие ограничения
%могут включать битовые операции). Подобный решатель был разработан в
%IBM для инструмента Genesys-Pro~\cite{GenesysSolver}. Однако
%создание такого решателя -- отдельное сложное исследование, которое
%не входило в цели данного исследования. В данной работе было принято
%решение использовать доступные существующие решатели (не обязательно
%CSP) и сосредоточиться на упрощении генерируемых ограничений для
%некоторых частных случаев архитектур.
%
%%\begin{figure}[h]
%%\parbox{0.5\textwidth}{ \centering
%%  \includegraphics[width=0.45\textwidth]{3.impl/genesys-pro}
%%} \vline
%%\parbox{0.5\textwidth}{ \centering
%%  \includegraphics[width=0.45\textwidth]{3.impl/mygen}
%%}
%%\caption{Сравнение с Genesys-Pro}\label{comparison_genesyspro}
%%\end{figure}
%
%В отличие от Genesys-Pro в предлагаемом инструменте описание
%семантики инструкций задается в едином виде -- в виде описаний
%тестовых ситуаций~\cite{my_syrcose_2008, my_isp_2008}. Каждая
%тестовая ситуация описывает не только ограничение на свои аргументы,
%но и результат исполнения инструкции \emph{при данном ограничении на
%аргументы} инструкции декларативным образом. В функции, которую
%реализует инструкция, выделяются отдельные \emph{ветви
%функциональности}, ситуации различного поведения инструкций, каждая
%ветвь функциональности становится отдельной тестовой ситуацией.
%Например, инструкция целочисленного сложения ADD может быть
%исполнена либо точно, либо с возникновением переполнения. Поэтому у
%этой инструкции можно выделить 2 ветви функциональности (точное
%исполнение и исполнение с переполнением), каждая ветвь дает свою
%тестовую ситуацию.

\section{Сравнение с работами Intel}

В ряде публикаций~\cite{MicroFORMAL} описывается инструмент MicroFORMAL, разрабатываемый в Intel. Он используется для некоторых задач формальной верификации разрабатываемых микропроцессоров (в частности, для проверки обратной совместимости). В рамках этой работы требуется описывать поведение микропроцессоров, формализовывать инструкции. Авторы статей упоминают \emph{IRL-представление} микрокода (IRL --- Intermediate Representation Language). Спецификация на IRL описывает функциональность инструкции и побочный эффект (изменение <<внешних>> переменных). Ровно ту же цель преследуют и модели инструкций, предлаагемые в данной работе. Спецификация на IRL представляет собой последовательность операторов (эта же идея используется здесь).

IRL включает в себя управляющие операторы (\texttt{if}, \texttt{goto}), поскольку верификация с использованием спецификаций на IRL нацелена в первую очередь на верификацию потоков управления. В данной работе поток управления не предполагает подобных операторов.

IRL позволяет описывать инструкции обращения к памяти. Однако в нем используется только плоская модель памяти (т.е. память как одномерный массив ячеек) с возможностью обращения <<по индексу>>. Напротив, модели инструкций, предлагаемые в данной работе, позволяют описывать работу с памятью более детально, с указанием успешности обращений в различные блоки подсистемы управления памяти. 
